perm filename LIS5.PPL[VLI,LSP] blob sn#382018 filedate 1978-09-08 generic text, type C, neo UTF8
COMMENT āŠ—   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	(TML)
C00003 ENDMK
CāŠ—;
(TML)

  %We now set up a simple tactic for proving the associativity of
   APPEND, and do the proof.
  %


let ss = itlist ssadd [APPENDUUthm; APPENDNILthm; APPENDCONSthm] 
                BASICSS;;

let TAC = LISTINDUCTAC"L:list" THEN SIMPTAC ;;

"APPEND(APPEND L M) N == APPEND L (APPEND M N)" ;;

let (),proof = TAC(it, ss, []);;

proof[];;
hyp(proof[]);;